\documentclass{article}
\usepackage[a4paper,margin=2cm,top=2.0cm,bottom=2.34cm]{geometry}
\usepackage[spanish,activeacute]{babel}
\usepackage{algo2symb}
\usepackage{newalgo}
%\usepackage{tad}

\parskip=1.5ex
\pagestyle{empty}

\newcommand\interfaz[5]{\noindent \\#1\ifblank{#2}\then{}\else{($#2$)}\fi \ifblank{#3}\then{}\else{$\rightarrow$ $#3$}\fi \\ \{$#4$\} \\ \{$#5$\}}
\newcommand\estr[2]{#1 src estr\_#1 donde estr\_#1 es:\\ #2}
\newcommand\rep[2]{Rep: estr\_#1 $\rightarrow$ bool\\ Rep(e) = #2}
\newcommand\abs[3]{Abs:estr\_ #1 e $\rightarrow$ #1 Rep(e)\\ Abs(e) = #2 / \\ #3}
\newcommand\complejidad[1]{\noindent \comentario{Complejidad: \Ode{#1}}}
%\newcommand\dupla[2]{$<$ #1 $\times$ #2 $>$}
%\newcommand\trupla[3]{$<$ #1 $\times$ #2 $\times$ #3 $>$}

\begin{document}

\noindent \textbf{Modulo lista($\alpha$)}

\noindent Se explica con la especificacion de secu($\alpha$) e iterSecu($\alpha$)\\
\textbf{usa:} puntero \\
\textbf{generos:} lista($\alpha$)

\noindent \textbf{Interfaz}

\complejidad{1}
\interfaz{Nueva}{}{res:lista(\alpha)}{true}{res \igobs <>}

\complejidad{1}
\interfaz{Agregar}{\param{in}{e}{\alpha}, \param{inout}{l}{Lista(\alpha)}}{}{l \igobs {l}_{0}}{l \igobs e \bullet {l}_{0}}

\complejidad{1}
\interfaz{EsVacia}{\param{in}{l}{Lista(\alpha)}}{res:bool}{true}{res \igobs vacia?(l)}

\complejidad{1}
\interfaz{Primero}{\param{in}{l}{Lista(\alpha)}}{res:\alpha}{\neg vacia?(l)}{res \igobs prim(l)}

\noindent \comentario{Complejidad: O(1). Devuelve por aliasing}
\interfaz{Fin}{\param{in}{l}{Lista(\alpha)}}{res:Lista(\alpha)}{\neg vacia?(l)}{res \igobs fin(l)}

\noindent \comentario{Complejidad: O(1).}
\interfaz{Ultimo}{\param{in}{l}{Lista(\alpha)}}{res:\alpha}{\neg vacia?(l)}{res \igobs ult(l)}


\complejidad{1}
\interfaz{AgregarAtras}{\param{in}{e}{\alpha}, \param{inout}{l}{Lista(\alpha)}}{}{l \igobs {l}_{0}}{l \igobs {l}_{0} \bullet e}

\noindent \comentario{Complejidad: O(n), donde n es la cantidad de elementos en la lista}
\interfaz{Esta}{\param{in}{e}{\alpha}, \param{in}{l}{Lista(\alpha)}}{res:bool}{true}{res \igobs esta?(e,{l}_{0})}

\complejidad{1}
\interfaz{Eliminar}{\param{inout}{it}{iterLista(\alpha)}}{}{{l}_{0} \igobs VerSecu(it) \wedge {i}_{o} \igobs VerSecuSuby(it) \wedge \neg Vacia({i}_{0})}{VerSecuSuby(it) \igobs  Fin({i}_{0})\wedge VerSecu(it) \igobs take({l}_{0},long({l}_{0})-long({i}_{0})) \&\& Fin({i}_{0})}

\complejidad{1}
\interfaz{Longitud}{\param{in}{l}{Lista(\alpha)}}{res: nat}{true}{res \igobs long(l)}

\noindent \comentario{Complejidad: O(n), donde n es la cantidad de elementos en la lista}
\interfaz{Iesimo}{\param{in}{i}{nat}, \param{in}{l}{Lista(\alpha)}}{res: \alpha}{i < long(l)}{res \igobs Iesimo(i,l)}

\complejidad{1}
\interfaz{CrearIt}{\param{in}{l}{Lista(\alpha)}}{res: iterLista(\alpha)}{true}{res \igobs CrearIt(l,l)}

\complejidad{1}
\interfaz{CrearItAlUlt}{\param{in}{l}{Lista(\alpha)}}{res: iterLista(\alpha)}{true}{res \igobs CrearIt(l,ult(l) \bullet <>)}

\noindent \comentario{Complejidad: O(1). Devuelve por aliasing}
\interfaz{Lista}{\param{in}{it}{iterLista(\alpha)}}{res: lista(\alpha)}{true}{res \igobs VerSecu(it)}

\complejidad{1}
\interfaz{Actual}{\param{in}{it}{iterLista(\alpha)}}{res: \alpha}{\neg vacia?(VerSecuSuby(it))}{res \igobs prim(VerSecuSuby(it))}

\complejidad{1}
\interfaz{TieneProximo}{\param{in}{it}{iterLista(\alpha)}}{res: bool}{true}{res \igobs \neg vacia?(VerSecuSuby(it))}

\complejidad{1}
\interfaz{Avanzar}{\param{inout}{it}{iterLista(\alpha)}}{}{it \igobs {it}_{0} \wedge \neg vacia?(VerSecuSuby(it))}{VerSecu(it) \igobs VerSecu({it}_{0}) \wedge VerSecuSuby(it) \igobs Fin(VerSecuSuby({it}_{0}))}

\noindent \textbf{Estructura}

\noindent \estr{lista($\alpha$)}{\trupla{primero: puntero(nodo)}{ultimo: puntero(nodo)}{longitud: nat}}
donde nodo es: \\ \trupla{anterior: puntero(nodo)}{valor: $\alpha$}{proximo: puntero(nodo)}

\noindent \estr{iterLista($\alpha$)}{\dupla{lista: puntero(estr\_lista($\alpha$))}{pos: puntero(nodo)}}

\noindent \textbf{Invariante de representacion}

\noindent \rep{lista($\alpha$)}{(e.primero = nil $\wedge$ e.ultimo = nil $\wedge$ longitud = 0) $\oluego$ (*(e.primero).anterior = nil $\wedge$ *(e.ultimo).proximo = nil $\wedge$ deUnExtremoLlegoAlOtro)} \\ \\
deUnExtremoLlegoAlOtro = \textit{empezando del nodo apuntado por $'$primero$'$ y siguiendo la cadena de nodos mediante el puntero $'$proximo$'$ (mientras este no sea nil), se llega en una cantidad finita de pasos al nodo apuntado por $'$ultimo$'$ y la cantidad de nodos recorrida es $'$longitud$'$. Del mismo modo se puede recorrer desde $'$ultimo$'$ a $'$primero$'$ mediante el puntero $'$anterior$'$)}

\noindent \rep{iterLista($\alpha$)}{\textit{el nodo *pos es parte de la cadena de nodos de la lista *lista.}}

\noindent \textbf{Funcion de abstraccion}

\noindent \abs{lista($\alpha$)}{l}{EsVacia(e) $\igobs$ vacia?(l) $\wedge$ $\neg$ vacia(l) $\Rightarrow_L$ (*(e.primero) $\igobs$ Primero(l) $\wedge$ $<*(e.primero).proximo \times e.ultimo>$ $\igobs$ Fin(l))}

\noindent \abs{iterLista($\alpha$)}{it}{verSecu(it) $\igobs$ Abs(*(e.lista)) $\wedge$ verSecuSuby(it) $\igobs$ $<primero: e.pos \times ultimo: *(e.lista).ultimo \times longitud: *(e.lista).longitud-posIterador>$}

\noindent \textbf{Algoritmos} \\

\begin{algorithm}{iNueva}{}{res\!:estr\_lista}
	res \= $\trupla{nil}{nil}{0}$
\end{algorithm}

\begin{algorithm}{iAgregar}{\param{in}{a}{\alfa}, \param{inout}{e}{estr\_lista}}{}
	*(e.primero).anterior \= \& $\trupla{nil}{a}{e.primero}$\\
	e.primero \= *(e.primero).anterior \\
	e.longitud++
\end{algorithm}

\begin{algorithm}{iEsVacia}{\param{in}{l}{estr\_lista}}{res\!:bool}
	res \= l.primero = nil
\end{algorithm}

\begin{algorithm}{iPrimero}{\param{in}{l}{estr\_lista}}{res\!:\alfa}
	res \= *(l.primero).valor
\end{algorithm}

\begin{algorithm}{iFin}{\param{in}{l}{estr\_lista}}{res\!:estr\_lista}
	res \= $\trupla{*(l.primero).proximo}{l.ultimo}{l.longitud-1}$
\end{algorithm}\\

\begin{algorithm}{iUltimo}{\param{in}{l}{estr\_lista}}{res\!:\alfa}
	res \= *(l.ultimo).valor
\end{algorithm}

\begin{algorithm}{iAgregarAtras}{\param{in}{a}{\alfa}, \param{inout}{l}{estr\_lista}}{}
	*(l.ultimo).proximo \= \&$\trupla{l.ultimo}{a}{nil}$\\
	l.ultimo \= *(l.ultimo).proximo \\
	l.longitud++
\end{algorithm}

\begin{algorithm}{iEsta}{\param{in}{a}{\alfa}, \param{in}{l}{estr\_lista}}{res\!: bool}
	res: bool \= false\\
	actual: puntero(nodo) \= l.primero\\
	\begin{WHILE}{actual \neq nil \wedge \neg res}
		\begin{IF}{*actual.valor = a}
			res \= true
		\end{IF}\\
		actual \= *actual.proximo
	\end{WHILE}
\end{algorithm}

\noindent \textit{\small{Si $"$a$"$ es el ultimo elemento de la lista el while se ejecuta tantas veces como la longitud de la lista. Como las asignaciones y evaluar la guarda del if cuestan O(1) entonces el while cuesta n*k donde k es una constante, es decir la complejidad es O(n).}}\\

\begin{algorithm}{iEliminar}{\param{in}{it}{iterLista(\alfa)}}{}
	\begin{IF}{*(it.pos).anterior \neq nil}
		*(*(it.pos).anterior).proximo \= *(it.pos).proximo
	\ELSE
		*(it.lista).primero \= *(it.pos).proximo \\
		*(*(it.lista).primero).anterior \= nil
	\end{IF} \\
	\begin{IF}{*(it.pos).proximo \neq nil}
		*(*(it.pos).proximo).anterior \= *(it.pos).anterior
	\ELSE
		*(it.lista).ultimo \= *(it.pos).anterior \\
		*(*(it.lista).ultimo).siguiente \= nil
	\end{IF} \\
	*(it.lista).longitud--\\
	iAvanzar(it)
\end{algorithm}

\begin{algorithm}{iLongitud}{\param{in}{l}{estr\_lista}}{res\!: nat}
	res \= l.longitud
\end{algorithm}

\begin{algorithm}{iIesimo}{\param{in}{i}{nat}, \param{in}{l}{estr\_lista}}{res\!:\alfa}
	j: nat \= 0 \\
	pos: puntero(nodo) \= l.primero\\
		\begin{WHILE}{j<i}
			pos \= *pos.proximo\\
			j++
		\end{WHILE} \\
	res \= *pos.valor
\end{algorithm}

\noindent \textit{\small{Si la posici'on buscada es la ultima de la lista el while se ejecuta tantas veces como la longitud de la misma. Como las asignaciones cuestan O(1) entonces el while cuesta n*k, donde k es una constante, es decir la complejidad es O(n).}}\\

\begin{algorithm}{iCrearIt}{\param{in}{l}{estr\_lista}}{res\!: estr\_iter}
	res \= $\dupla{\&l}{l.primero}$
\end{algorithm}

\begin{algorithm}{iCrearItAlUlt}{\param{in}{l}{estr\_lista}}{res\!: estr\_iter}
	res \= $\dupla{\&l}{l.ultimo}$
\end{algorithm}

\begin{algorithm}{iLista}{\param{in}{it}{estr\_iter}}{res\!: estr\_lista(\alfa)}
	res \= *(it.lista)
\end{algorithm}


\begin{algorithm}{iActual}{\param{in}{it}{estr\_iter}}{res\!: \alfa}
	res \= *(it.pos).valor
\end{algorithm}

\begin{algorithm}{iTieneProximo}{\param{in}{it}{estr\_iter}}{res\!: bool}
	res \= *(it.pos).proximo \neq nil
\end{algorithm}

\begin{algorithm}{iAvanzar}{\param{inout}{it}{estr\_iter}}{}
	it.pos \= *(it.pos).proximo
\end{algorithm}

\end{document}
